﻿using System;
using System.Collections.Generic;
using System.Text;
using Microsoft.Cci;
using Microsoft.Cci.MutableCodeModel;
using System.IO;
using System.Runtime.Serialization.Formatters.Binary;

namespace Tool
{
    class AssumptionAdder : CodeMutator
    {
        private Boolean MCDC = true;
        public int counter;

        public int count()
        {
            return counter;
        }

        
        public AssumptionAdder(IMetadataHost host, ISourceLocationProvider/*?*/ sourceLocationProvider)
            : base(host, sourceLocationProvider)
        {
            counter = 0;
        }

        public override IBlockStatement Visit(BlockStatement blockStatement)
        {
            List<IStatement> statements = blockStatement.Statements;
            List<IStatement> newList = new List<IStatement>();
            foreach (var statement in statements)
            {
                IExpressionStatement expression = statement as IExpressionStatement;
                if (expression != null)
                {
                    IAssignment assign = expression.Expression as IAssignment;
                    if (assign != null)
                    {
                        Statement constraint = ExtractCondition(assign);

                        if (constraint != CodeDummy.Block)
                        {
                            if (constraint as BlockStatement != null)
                            {
                                newList.AddRange((constraint as BlockStatement).Statements);
                            }
                            else
                            {
                                newList.Add(constraint);
                            }
                        }
                    }

                }
                IConditionalStatement conditional = statement as IConditionalStatement;
                if (conditional != null)
                {
                    Statement constraint = getConstraints(conditional);
                    if (constraint != CodeDummy.Block)
                    {
                        if (constraint as BlockStatement != null)
                        {
                            newList.AddRange((constraint as BlockStatement).Statements);
                        }
                        else
                        {
                            newList.Add(constraint);
                        }
                    }
                }
                IReturnStatement retStmt = statement as IReturnStatement;
                if (retStmt != null)
                {
                    Statement constraint = ExtractCondition(retStmt.Expression);
                    if (constraint != CodeDummy.Block)
                    {
                        if (constraint as BlockStatement != null)
                        {
                            newList.AddRange((constraint as BlockStatement).Statements);
                        }
                        else
                        {
                            newList.Add(constraint);
                        }
                    }
                }

                newList.Add(statement);
            }
            blockStatement.Statements = newList;
            blockStatement.Statements = Visit(blockStatement.Statements);
            return blockStatement;
        }

        private Statement getConstraints(IConditionalStatement conditionalStatement)
        {
            Statement statement = ExtractCondition(conditionalStatement.Condition as IExpression);
            return statement;
        }

        private Statement ExtractCondition(IExpression expression)
        {

            if (expression as GreaterThan != null)
            {
                IStatement stmt = Traverse(expression as GreaterThan);
                return stmt as Statement;

            }
            else if (expression as LessThan != null)
            {
                IStatement stmt = Traverse(expression as LessThan);
                return stmt as Statement;

            }
            else if (expression as LogicalNot != null)
            {
                IStatement stmt = Traverse(expression as LogicalNot);
                return stmt as Statement;

            }
            else if (expression as Conditional != null)
            {
                List<IExpression> clauseList = ExtractClauses(expression as Conditional);
                List<IExpression> clauseList2 = new List<IExpression>();
                clauseList2.AddRange(clauseList);
                IStatement stmt;
                if (MCDC)
                {
                    stmt = TraverseMCDC(expression as Conditional, clauseList);
                }
                else
                {
                    stmt = Traverse(clauseList);
                }


                List<IStatement> stmtList = new List<IStatement>();
                BlockStatement logicalCond = stmt as BlockStatement;
                if(logicalCond != null)
                    stmtList.AddRange(logicalCond.Statements);
                
                foreach (IExpression exp in clauseList2)
                {
                    BlockStatement blkstmt = ExtractCondition(exp) as BlockStatement;
                    if (blkstmt != null)
                        stmtList.AddRange(blkstmt.Statements);
                }

                BlockStatement bstatement = new BlockStatement();
                bstatement.Statements.AddRange(stmtList);
                stmt = bstatement as IStatement;

                return stmt as Statement;
            }
            else if (expression as Equality != null)
            {
                IStatement stmt = Traverse(expression as Equality);
                return stmt as Statement;
            }
            else if (expression as LessThanOrEqual != null)
            {
                GreaterThan gt = new GreaterThan();
                gt.LeftOperand = (expression as LessThanOrEqual).LeftOperand;
                gt.RightOperand = (expression as LessThanOrEqual).RightOperand;
                IStatement stmt = Traverse(gt);
                return stmt as Statement;
            }
            else if (expression as GreaterThanOrEqual != null)
            {
                LessThan lt = new LessThan();
                lt.LeftOperand = (expression as GreaterThanOrEqual).LeftOperand;
                lt.RightOperand = (expression as GreaterThanOrEqual).RightOperand;
                IStatement stmt = Traverse(lt);
                return stmt as Statement;
            }
            return new AssumeStatement() as Statement;
        }



        private IStatement TraverseMCDC(Conditional condition, List<IExpression> clauseList)
        {

            Conditional expression = new Conditional(condition as IConditional);

            List<IStatement> statementList = new List<IStatement>();

            CompileTimeConstant trueValue = new CompileTimeConstant();
            trueValue.Value = true;
            trueValue.Type = this.host.PlatformType.SystemBoolean;

            CompileTimeConstant falseValue = new CompileTimeConstant();
            falseValue.Value = false;
            falseValue.Type = this.host.PlatformType.SystemBoolean;

            for (int i = 0; i < clauseList.Count; i++)
            {
                Expression exp = clauseList[i] as Expression;

                Conditional expTrue = Utility.copy(expression as IExpression) as Conditional;

                Conditional expFalse = Utility.copy(expression as IExpression) as Conditional;


                expTrue = ReplaceClauses(expTrue, exp, trueValue as Expression);
                expFalse = ReplaceClauses(expFalse, exp, falseValue as Expression);

                NotEquality eq = new NotEquality();
                eq.RightOperand = expTrue;
                eq.LeftOperand = expFalse;

                ConditionalStatement condStatement = new ConditionalStatement();
                condStatement.Condition = eq;

                ConditionalStatement condStatement1 = new ConditionalStatement();
                condStatement1.Condition = exp;
                condStatement1.TrueBranch = new EmptyStatement();
                condStatement1.FalseBranch = new EmptyStatement();

                condStatement.TrueBranch = condStatement1 as IStatement;

                condStatement.FalseBranch = new EmptyStatement();

                statementList.Add(condStatement as IStatement);

            }
            BlockStatement blk = new BlockStatement();
            blk.Statements = statementList;
            return blk as IStatement;
        }

        private Conditional ReplaceClauses(Conditional conditional, Expression exp, Expression truthValue)
        {
            IExpression condition = conditional.Condition;

            if (condition as LogicalNot != null)
            {
                condition = (condition as LogicalNot).Operand;
                if (Utility.Equals(condition, exp))
                {
                    LogicalNot not = new LogicalNot();
                    not.Operand = truthValue;
                    conditional.Condition = not;
                }
                else if (condition as Conditional != null)
                {
                    LogicalNot not = new LogicalNot();
                    not.Operand = ReplaceClauses(condition as Conditional, exp, truthValue);
                    conditional.Condition = not;
                }

            }
            else if (condition as Conditional != null)
            {
                conditional.Condition = ReplaceClauses(condition as Conditional, exp, truthValue);
            }
            else if (Utility.Equals(condition, exp))
            {
                conditional.Condition = truthValue;
            }

            IExpression resultIfTrue = conditional.ResultIfTrue;

            if (resultIfTrue as LogicalNot != null)
            {
                resultIfTrue = (resultIfTrue as LogicalNot).Operand;
                if (Utility.Equals(resultIfTrue, exp))
                {
                    LogicalNot not = new LogicalNot();
                    not.Operand = truthValue;
                    conditional.ResultIfTrue = not;
                }
                else if (resultIfTrue as Conditional != null)
                {
                    LogicalNot not = new LogicalNot();
                    not.Operand = ReplaceClauses(resultIfTrue as Conditional, exp, truthValue);
                    conditional.ResultIfTrue = not;
                }
            }
            else if (resultIfTrue as Conditional != null)
            {
                conditional.ResultIfTrue = ReplaceClauses(resultIfTrue as Conditional, exp, truthValue);
            }
            else if (Utility.Equals(resultIfTrue, exp))
            {
                conditional.ResultIfTrue = truthValue;
            }


            IExpression resultIfFalse = conditional.ResultIfFalse;
            if (resultIfFalse as LogicalNot != null)
            {
                resultIfFalse = (resultIfFalse as LogicalNot).Operand;
                if (Utility.Equals(resultIfFalse, exp))
                {
                    LogicalNot not = new LogicalNot();
                    not.Operand = truthValue;
                    conditional.ResultIfFalse = not;
                }
                else if (resultIfFalse as Conditional != null)
                {
                    LogicalNot not = new LogicalNot();
                    not.Operand = ReplaceClauses(resultIfFalse as Conditional, exp, truthValue);
                    conditional.ResultIfFalse = not;
                }
            }
            else if (resultIfFalse as Conditional != null)
            {
                conditional.ResultIfFalse = ReplaceClauses(resultIfFalse as Conditional, exp, truthValue);
            }
            else if (Utility.Equals(resultIfFalse, exp))
            {
                conditional.ResultIfFalse = truthValue;
            }
            return conditional;
        }

        private IStatement Traverse(List<IExpression> clauseList)
        {
            BlockStatement block = new BlockStatement();
            List<IStatement> stmntList = new List<IStatement>();

            LocalDeclarationStatement localDeclare = new LocalDeclarationStatement();

            LocalDefinition localDef = new LocalDefinition();
            localDef.Name = this.host.NameTable.GetNameFor("aaaaaaaaaaaa");
            localDef.Type = this.host.PlatformType.SystemBoolean;
            localDeclare.LocalVariable = localDef;

            CompileTimeConstant initialValue = new CompileTimeConstant();
            initialValue.Value = true;
            initialValue.Type = this.host.PlatformType.SystemBoolean;

            localDeclare.InitialValue = initialValue;

            List<IStatement> tempBuffer = new List<IStatement>();
            tempBuffer.Add(localDeclare);

            BoundExpression tempvar = new BoundExpression();
            tempvar.Type = this.host.PlatformType.SystemBoolean;
            tempvar.Definition = localDef;

            TargetExpression holder = new TargetExpression();
            holder.Type = this.host.PlatformType.SystemBoolean;
            holder.Definition = localDef;

            BuildConditions(clauseList, stmntList, tempBuffer, tempvar, holder);
            block.Statements = stmntList;
            return block as IStatement;
        }

        private void BuildConditions(List<IExpression> clauseList, List<IStatement> stmntList,
            List<IStatement> tempBuffer, BoundExpression tempvar, TargetExpression holder)
        {
            IExpression predicate = clauseList[0];
            clauseList.Remove(predicate);
            List<IExpression> clauseList1 = new List<IExpression>();
            clauseList1.AddRange(clauseList);

            CompileTimeConstant cons = new CompileTimeConstant();
            cons.Value = false;
            cons.Type = this.host.PlatformType.SystemBoolean;

            CompileTimeConstant cons1 = new CompileTimeConstant();
            cons1.Value = true;
            cons1.Type = this.host.PlatformType.SystemBoolean;

            Equality eq = new Equality();
            eq.LeftOperand = predicate;
            eq.RightOperand = cons1;

            Conditional conditionalTrue = new Conditional();
            conditionalTrue.Condition = tempvar as IExpression;
            conditionalTrue.ResultIfFalse = cons;
            conditionalTrue.ResultIfTrue = eq;

            ExpressionStatement statement = new ExpressionStatement();
            Assignment assignment = new Assignment();
            assignment.Target = holder;
            assignment.Source = conditionalTrue as IExpression;
            statement.Expression = assignment as IExpression;
            tempBuffer.Add(statement);

            if (clauseList1.Count != 0)
            {
                BuildConditions(clauseList1, stmntList, tempBuffer, tempvar, holder);
            }
            else
            {
                stmntList.AddRange(tempBuffer);
                stmntList.Add(GetConstraint(tempvar as IExpression));
            }
            tempBuffer.Remove(statement);
            clauseList1.RemoveRange(0, clauseList1.Count);
            clauseList1.AddRange(clauseList);
            Equality eq2 = new Equality();
            eq2.LeftOperand = predicate;
            eq2.RightOperand = cons;

            Conditional conditionalFalse = new Conditional();
            conditionalFalse.Condition = tempvar as IExpression;
            conditionalFalse.ResultIfFalse = cons;
            conditionalFalse.ResultIfTrue = eq2;

            ExpressionStatement statement2 = new ExpressionStatement();
            Assignment assignment2 = new Assignment();
            assignment2.Target = holder;
            assignment2.Source = conditionalFalse as IExpression;
            statement2.Expression = assignment2 as IExpression;
            tempBuffer.Add(statement2);

            if (clauseList1.Count != 0)
            {
                BuildConditions(clauseList1, stmntList, tempBuffer, tempvar, holder);
            }
            else
            {
                stmntList.AddRange(tempBuffer);
                stmntList.Add(GetConstraint(tempvar as IExpression));
            }
            tempBuffer.Remove(statement2);
        }

        private IStatement Traverse(Equality equality)
        {
            BlockStatement block = new BlockStatement();
            List<IStatement> stmntList = new List<IStatement>();

            if (equality.LeftOperand as IExpression != null)
            {
                IStatement stmnt = ExtractCondition(equality.LeftOperand) as IStatement;
                if (stmnt as BlockStatement != null)
                    return stmnt;
            }

            Boolean isnumerical = false;
            if (equality.RightOperand.Type.ToString() == ("System.Int32"))
                isnumerical = true;

            if (isnumerical)
            {
                CompileTimeConstant cons = new CompileTimeConstant();
                cons.Value = 1;

                Addition add = new Addition();
                add.LeftOperand = equality.RightOperand;
                add.RightOperand = cons;

                Subtraction sub = new Subtraction();
                sub.LeftOperand = equality.RightOperand;
                sub.RightOperand = cons;

                Equality eq = new Equality();
                eq.LeftOperand = equality.LeftOperand;
                eq.RightOperand = add;
                //stmntList.Add(GetConstraint(eq as IExpression));
                ConditionalStatement cnd1 = GetConstraint(eq as IExpression) as ConditionalStatement;

                Equality eq2 = new Equality();
                eq2.LeftOperand = equality.LeftOperand;
                eq2.RightOperand = sub;
                //stmntList.Add(GetConstraint(eq2 as IExpression));
                ConditionalStatement cnd2 = GetConstraint(eq2 as IExpression) as ConditionalStatement;
                cnd1.FalseBranch = cnd2 as IStatement;

                Equality eq3 = new Equality();
                eq3.LeftOperand = equality.LeftOperand;
                eq3.RightOperand = equality.RightOperand;
                //stmntList.Add(GetConstraint(eq3 as IExpression));
                ConditionalStatement cnd3 = GetConstraint(eq3 as IExpression) as ConditionalStatement;
                cnd2.FalseBranch = cnd3 as IStatement;

                stmntList.Add(cnd1);
                block.Statements = stmntList;


            }
            return block as IStatement;
        }

        private IStatement Traverse(LogicalNot logicalNot)
        {
            Statement stmt = ExtractCondition(logicalNot.Operand as Expression);
            return stmt as IStatement;
        }

        private List<IExpression> ExtractClauses(Conditional conditional)
        {
            List<IExpression> clauseList = new List<IExpression>();
            IExpression condition = conditional.Condition;
            if (condition as LogicalNot != null)
            {
                condition = (condition as LogicalNot).Operand;
            }

            if (condition as Conditional != null)
            {
                clauseList.AddRange(ExtractClauses(condition as Conditional));
            }
            else
            {
                clauseList.Add(condition);
            }
            IExpression resultIfTrue = conditional.ResultIfTrue;
            if (resultIfTrue as LogicalNot != null)
            {
                resultIfTrue = (resultIfTrue as LogicalNot).Operand;
            }

            IExpression resultIfFalse = conditional.ResultIfFalse;
            if (resultIfFalse as LogicalNot != null)
            {
                resultIfFalse = (resultIfFalse as LogicalNot).Operand;
            }

            if (resultIfTrue as CompileTimeConstant == null)
            {
                if (resultIfTrue as Conditional != null)
                {
                    clauseList.AddRange(ExtractClauses(resultIfTrue as Conditional));
                }
                else
                {
                    clauseList.Add(resultIfTrue);
                }
            }
            if (resultIfFalse as CompileTimeConstant == null)
            {
                if (resultIfFalse as Conditional != null)
                {
                    clauseList.AddRange(ExtractClauses(resultIfFalse as Conditional));
                }
                else
                {
                    clauseList.Add(resultIfFalse);
                }
            }
            return clauseList;
        }

        /*
         * Exctacting Conditons from "a > b" expression, i.e.,
         * (a == b+1)||(a > b+1)||(a == b)||(a < b)
         */
        private IStatement Traverse(GreaterThan greaterThan)
        {
            BlockStatement block = new BlockStatement();
            List<IStatement> stmntList = new List<IStatement>();

            CompileTimeConstant cons = new CompileTimeConstant();
            cons.Value = 1;


            Addition add = new Addition();
            add.LeftOperand = greaterThan.RightOperand;
            add.RightOperand = cons;

            // a == b+1
            Equality eq = new Equality();
            eq.LeftOperand = greaterThan.LeftOperand;
            eq.RightOperand = add;

            ConditionalStatement cnd1 = GetConstraint(eq as IExpression) as ConditionalStatement;
            //stmntList.Add(GetConstraint(eq as IExpression));

            // a == b
            Equality eq2 = new Equality();
            eq2.LeftOperand = greaterThan.LeftOperand;
            eq2.RightOperand = greaterThan.RightOperand;

            //stmntList.Add(GetConstraint(eq2 as IExpression));
            ConditionalStatement cnd2 = GetConstraint(eq2 as IExpression) as ConditionalStatement;
            cnd1.FalseBranch = cnd2 as IStatement;

            // a > b+1
            GreaterThan gt = new GreaterThan();
            gt.LeftOperand = greaterThan.LeftOperand;
            gt.RightOperand = add;

            //stmntList.Add(GetConstraint(gt as IExpression));
            ConditionalStatement cnd3 = GetConstraint(gt as IExpression) as ConditionalStatement;
            cnd2.FalseBranch = cnd3 as IStatement;
            // a < b
            LessThan lt = new LessThan();
            lt.LeftOperand = greaterThan.LeftOperand;
            lt.RightOperand = greaterThan.RightOperand;

            //stmntList.Add(GetConstraint(lt as IExpression));
            ConditionalStatement cnd4 = GetConstraint(lt as IExpression) as ConditionalStatement;
            cnd3.FalseBranch = cnd4 as IStatement;

            stmntList.Add(cnd1 as IStatement);

            block.Statements = stmntList;
            return block as IStatement;
        }

        private IStatement GetConstraint(IExpression expression)
        {
            ConditionalStatement cndstmt = new ConditionalStatement();
            cndstmt.Condition = expression;
            cndstmt.TrueBranch = new EmptyStatement();
            cndstmt.FalseBranch = new EmptyStatement();
            return cndstmt as IStatement;
        }

        /*
         * Exctacting Conditons from "a < b" expression, i.e.,
         * (a == b-1)||(a < b-1)||(a == b)||(a > b)
         */
        private IStatement Traverse(LessThan lessThan)
        {
            BlockStatement block = new BlockStatement();
            List<IStatement> stmntList = new List<IStatement>();

            CompileTimeConstant cons = new CompileTimeConstant();
            cons.Value = 1;

            Subtraction sub = new Subtraction();
            sub.LeftOperand = lessThan.RightOperand;
            sub.RightOperand = cons;

            Equality eq = new Equality();
            eq.LeftOperand = lessThan.LeftOperand;
            eq.RightOperand = sub;
            //stmntList.Add(GetConstraint(eq as IExpression));
            ConditionalStatement cnd1 = GetConstraint(eq as IExpression) as ConditionalStatement;

            // a < b-1
            LessThan lt = new LessThan();
            lt.LeftOperand = lessThan.LeftOperand;
            lt.RightOperand = sub;
            //stmntList.Add(GetConstraint(lt as IExpression));
            ConditionalStatement cnd2 = GetConstraint(lt as IExpression) as ConditionalStatement;
            cnd1.FalseBranch = cnd2 as IStatement;

            // a == b
            Equality eq2 = new Equality();
            eq2.LeftOperand = lessThan.LeftOperand;
            eq2.RightOperand = lessThan.RightOperand;
            //stmntList.Add(GetConstraint(eq2 as IExpression));
            ConditionalStatement cnd3 = GetConstraint(eq2 as IExpression) as ConditionalStatement;
            cnd2.FalseBranch = cnd3 as IStatement;

            // a > b
            GreaterThan gt = new GreaterThan();
            gt.LeftOperand = lessThan.LeftOperand;
            gt.RightOperand = lessThan.RightOperand;
            //stmntList.Add(GetConstraint(gt as IExpression));
            ConditionalStatement cnd4 = GetConstraint(gt as IExpression) as ConditionalStatement;
            cnd3.FalseBranch = cnd4 as IStatement;

            stmntList.Add(cnd1);

            block.Statements = stmntList;
            return block as IStatement;
        }
    }
}
